Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    half(0)  → 0
2:    half(s(0))  → 0
3:    half(s(s(x)))  → s(half(x))
4:    lastbit(0)  → 0
5:    lastbit(s(0))  → s(0)
6:    lastbit(s(s(x)))  → lastbit(x)
7:    conv(0)  → cons(nil,0)
8:    conv(s(x))  → cons(conv(half(s(x))),lastbit(s(x)))
There are 5 dependency pairs:
9:    HALF(s(s(x)))  → HALF(x)
10:    LASTBIT(s(s(x)))  → LASTBIT(x)
11:    CONV(s(x))  → CONV(half(s(x)))
12:    CONV(s(x))  → HALF(s(x))
13:    CONV(s(x))  → LASTBIT(s(x))
The approximated dependency graph contains 3 SCCs: {9}, {10} and {11}.
Tyrolean Termination Tool  (0.01 seconds)   ---  May 4, 2006